Nuprl Lemma : gcd_elim
2,24
postcript
pdf
a
,
b
:
.
y
:
. GCD(
a
;
b
;
y
) & gcd(
a
;
b
) =
y
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
gcd(
a
;
b
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
GCD(
a
;
b
;
y
)
,
Prop
Lemmas
gcd
sat
gcd
p
,
gcd
p
wf
,
gcd
wf
origin
a, b:
. 
y:. GCD(a;b;y) & gcd(a;b) = y a, b:. y:. GCD(a;b;y) & gcd(a;b) = y x:A. B(x)
Tx:A. B(x)